Skip to content

fix: introduce sum_diff_eq_zero_of_equal_combinations#14

Merged
ZRTMRH merged 2 commits into
ZRTMRH:mainfrom
JadAbouHawili:spacing-docs
Apr 18, 2026
Merged

fix: introduce sum_diff_eq_zero_of_equal_combinations#14
ZRTMRH merged 2 commits into
ZRTMRH:mainfrom
JadAbouHawili:spacing-docs

Conversation

@JadAbouHawili
Copy link
Copy Markdown

No description provided.

@JadAbouHawili
Copy link
Copy Markdown
Author

currently, sum_diff_eq_zero_of_equal_combinations is only mentioned in the hint and not present in the right side pane which the level directs the user towards to read about the necessary lemmas in level 7 of linear independence and span world

moreover , usage of (strict := true) here is a step in direction of resolving the repeated note:
"Note: This level may experience a hint display issue where hints repeat. If you see the same hint multiple times, the level is still working correctly - just continue with your proof as normal."

Judicious usage of (strict := true) for hints that suggest using obtain , by_cases , have or any other 'hypothesis introducing' tactic that doesn't change the goal will resolve repeated hint displays. You can refer to https://github.com/leanprover-community/lean4game/blob/main/doc/hints.md#5-strict-context-matching for some details

@ZRTMRH ZRTMRH merged commit 4aa9f91 into ZRTMRH:main Apr 18, 2026
1 check passed
@ZRTMRH
Copy link
Copy Markdown
Owner

ZRTMRH commented Apr 18, 2026

Thank you! Merged.

@JadAbouHawili JadAbouHawili deleted the spacing-docs branch April 18, 2026 19:12
@JadAbouHawili JadAbouHawili restored the spacing-docs branch April 18, 2026 19:12
@JadAbouHawili JadAbouHawili deleted the spacing-docs branch April 18, 2026 19:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants